The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(O(1), O(n^1)).

0 CpxTRS
↳1 CpxTrsToCdtProof (BOTH BOUNDS(ID, ID), 0 ms)
↳2 CdtProblem
    ↳3 CdtNarrowingProof (BOTH BOUNDS(ID, ID), 0 ms)
    ↳4 CdtProblem
    ↳5 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID), 0 ms)
    ↳6 CdtProblem
    ↳7 CdtNarrowingProof (BOTH BOUNDS(ID, ID), 13 ms)
    ↳8 CdtProblem
    ↳9 CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID), 0 ms)
    ↳10 CdtProblem
    ↳11 CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID), 7 ms)
    ↳12 CdtProblem
    ↳13 CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID), 0 ms)
    ↳14 CdtProblem
    ↳15 CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID), 0 ms)
    ↳16 CdtProblem
↳17 CpxTrsMatchBoundsTAProof (⇔, 0 ms)
↳18 BOUNDS(O(1), O(n^1))

(0) Obligation:

Runtime Complexity TRS:
The TRS R consists of the following rules:

p(a(x0), p(b(x1), p(a(x2), x3))) → p(x2, p(a(a(x0)), p(b(x1), x3)))

Rewrite Strategy: INNERMOST

(1) CpxTrsToCdtProof (BOTH BOUNDS(ID, ID) transformation)

Converted CpxTRS to CDT

(2) Obligation:

Complexity Dependency Tuples Problem
Rules:

p(a(z0), p(b(z1), p(a(z2), z3))) → p(z2, p(a(a(z0)), p(b(z1), z3)))
Tuples:

P(a(z0), p(b(z1), p(a(z2), z3))) → c(P(z2, p(a(a(z0)), p(b(z1), z3))), P(a(a(z0)), p(b(z1), z3)), P(b(z1), z3))
S tuples:

P(a(z0), p(b(z1), p(a(z2), z3))) → c(P(z2, p(a(a(z0)), p(b(z1), z3))), P(a(a(z0)), p(b(z1), z3)), P(b(z1), z3))
K tuples:none
Defined Rule Symbols:

p

Defined Pair Symbols:

P

Compound Symbols:

c

(3) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Use narrowing to replace P(a(z0), p(b(z1), p(a(z2), z3))) → c(P(z2, p(a(a(z0)), p(b(z1), z3))), P(a(a(z0)), p(b(z1), z3)), P(b(z1), z3)) by

P(a(x0), p(b(z1), p(a(x2), p(a(z2), z3)))) → c(P(x2, p(z2, p(a(a(a(x0))), p(b(z1), z3)))), P(a(a(x0)), p(b(z1), p(a(z2), z3))), P(b(z1), p(a(z2), z3)))
P(a(x0), p(b(x1), p(a(x2), x3))) → c

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

p(a(z0), p(b(z1), p(a(z2), z3))) → p(z2, p(a(a(z0)), p(b(z1), z3)))
Tuples:

P(a(x0), p(b(z1), p(a(x2), p(a(z2), z3)))) → c(P(x2, p(z2, p(a(a(a(x0))), p(b(z1), z3)))), P(a(a(x0)), p(b(z1), p(a(z2), z3))), P(b(z1), p(a(z2), z3)))
P(a(x0), p(b(x1), p(a(x2), x3))) → c
S tuples:

P(a(x0), p(b(z1), p(a(x2), p(a(z2), z3)))) → c(P(x2, p(z2, p(a(a(a(x0))), p(b(z1), z3)))), P(a(a(x0)), p(b(z1), p(a(z2), z3))), P(b(z1), p(a(z2), z3)))
P(a(x0), p(b(x1), p(a(x2), x3))) → c
K tuples:none
Defined Rule Symbols:

p

Defined Pair Symbols:

P

Compound Symbols:

c, c

(5) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)

Removed 1 trailing nodes:

P(a(x0), p(b(x1), p(a(x2), x3))) → c

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:

p(a(z0), p(b(z1), p(a(z2), z3))) → p(z2, p(a(a(z0)), p(b(z1), z3)))
Tuples:

P(a(x0), p(b(z1), p(a(x2), p(a(z2), z3)))) → c(P(x2, p(z2, p(a(a(a(x0))), p(b(z1), z3)))), P(a(a(x0)), p(b(z1), p(a(z2), z3))), P(b(z1), p(a(z2), z3)))
S tuples:

P(a(x0), p(b(z1), p(a(x2), p(a(z2), z3)))) → c(P(x2, p(z2, p(a(a(a(x0))), p(b(z1), z3)))), P(a(a(x0)), p(b(z1), p(a(z2), z3))), P(b(z1), p(a(z2), z3)))
K tuples:none
Defined Rule Symbols:

p

Defined Pair Symbols:

P

Compound Symbols:

c

(7) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Use narrowing to replace P(a(x0), p(b(z1), p(a(x2), p(a(z2), z3)))) → c(P(x2, p(z2, p(a(a(a(x0))), p(b(z1), z3)))), P(a(a(x0)), p(b(z1), p(a(z2), z3))), P(b(z1), p(a(z2), z3))) by

P(a(x0), p(b(z1), p(a(x2), p(a(x3), p(a(z2), z3))))) → c(P(x2, p(x3, p(z2, p(a(a(a(a(x0)))), p(b(z1), z3))))), P(a(a(x0)), p(b(z1), p(a(x3), p(a(z2), z3)))), P(b(z1), p(a(x3), p(a(z2), z3))))
P(a(x0), p(b(x1), p(a(x2), p(a(x3), x4)))) → c(P(a(a(x0)), p(b(x1), p(a(x3), x4))))

(8) Obligation:

Complexity Dependency Tuples Problem
Rules:

p(a(z0), p(b(z1), p(a(z2), z3))) → p(z2, p(a(a(z0)), p(b(z1), z3)))
Tuples:

P(a(x0), p(b(z1), p(a(x2), p(a(x3), p(a(z2), z3))))) → c(P(x2, p(x3, p(z2, p(a(a(a(a(x0)))), p(b(z1), z3))))), P(a(a(x0)), p(b(z1), p(a(x3), p(a(z2), z3)))), P(b(z1), p(a(x3), p(a(z2), z3))))
P(a(x0), p(b(x1), p(a(x2), p(a(x3), x4)))) → c(P(a(a(x0)), p(b(x1), p(a(x3), x4))))
S tuples:

P(a(x0), p(b(z1), p(a(x2), p(a(x3), p(a(z2), z3))))) → c(P(x2, p(x3, p(z2, p(a(a(a(a(x0)))), p(b(z1), z3))))), P(a(a(x0)), p(b(z1), p(a(x3), p(a(z2), z3)))), P(b(z1), p(a(x3), p(a(z2), z3))))
P(a(x0), p(b(x1), p(a(x2), p(a(x3), x4)))) → c(P(a(a(x0)), p(b(x1), p(a(x3), x4))))
K tuples:none
Defined Rule Symbols:

p

Defined Pair Symbols:

P

Compound Symbols:

c, c

(9) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID) transformation)

Use forward instantiation to replace P(a(x0), p(b(x1), p(a(x2), p(a(x3), x4)))) → c(P(a(a(x0)), p(b(x1), p(a(x3), x4)))) by

P(a(z0), p(b(z1), p(a(z2), p(a(z3), p(a(y3), p(a(y4), y5)))))) → c(P(a(a(z0)), p(b(z1), p(a(z3), p(a(y3), p(a(y4), y5))))))
P(a(z0), p(b(z1), p(a(z2), p(a(z3), p(a(y3), y4))))) → c(P(a(a(z0)), p(b(z1), p(a(z3), p(a(y3), y4)))))

(10) Obligation:

Complexity Dependency Tuples Problem
Rules:

p(a(z0), p(b(z1), p(a(z2), z3))) → p(z2, p(a(a(z0)), p(b(z1), z3)))
Tuples:

P(a(x0), p(b(z1), p(a(x2), p(a(x3), p(a(z2), z3))))) → c(P(x2, p(x3, p(z2, p(a(a(a(a(x0)))), p(b(z1), z3))))), P(a(a(x0)), p(b(z1), p(a(x3), p(a(z2), z3)))), P(b(z1), p(a(x3), p(a(z2), z3))))
P(a(z0), p(b(z1), p(a(z2), p(a(z3), p(a(y3), p(a(y4), y5)))))) → c(P(a(a(z0)), p(b(z1), p(a(z3), p(a(y3), p(a(y4), y5))))))
P(a(z0), p(b(z1), p(a(z2), p(a(z3), p(a(y3), y4))))) → c(P(a(a(z0)), p(b(z1), p(a(z3), p(a(y3), y4)))))
S tuples:

P(a(x0), p(b(z1), p(a(x2), p(a(x3), p(a(z2), z3))))) → c(P(x2, p(x3, p(z2, p(a(a(a(a(x0)))), p(b(z1), z3))))), P(a(a(x0)), p(b(z1), p(a(x3), p(a(z2), z3)))), P(b(z1), p(a(x3), p(a(z2), z3))))
P(a(z0), p(b(z1), p(a(z2), p(a(z3), p(a(y3), p(a(y4), y5)))))) → c(P(a(a(z0)), p(b(z1), p(a(z3), p(a(y3), p(a(y4), y5))))))
P(a(z0), p(b(z1), p(a(z2), p(a(z3), p(a(y3), y4))))) → c(P(a(a(z0)), p(b(z1), p(a(z3), p(a(y3), y4)))))
K tuples:none
Defined Rule Symbols:

p

Defined Pair Symbols:

P

Compound Symbols:

c, c

(11) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID) transformation)

Use forward instantiation to replace P(a(x0), p(b(z1), p(a(x2), p(a(x3), p(a(z2), z3))))) → c(P(x2, p(x3, p(z2, p(a(a(a(a(x0)))), p(b(z1), z3))))), P(a(a(x0)), p(b(z1), p(a(x3), p(a(z2), z3)))), P(b(z1), p(a(x3), p(a(z2), z3)))) by

P(a(z0), p(b(z1), p(a(a(y0)), p(a(z3), p(a(z4), z5))))) → c(P(a(y0), p(z3, p(z4, p(a(a(a(a(z0)))), p(b(z1), z5))))), P(a(a(z0)), p(b(z1), p(a(z3), p(a(z4), z5)))), P(b(z1), p(a(z3), p(a(z4), z5))))
P(a(z0), p(b(z1), p(a(z2), p(a(z3), p(a(z4), p(a(y4), y5)))))) → c(P(z2, p(z3, p(z4, p(a(a(a(a(z0)))), p(b(z1), p(a(y4), y5)))))), P(a(a(z0)), p(b(z1), p(a(z3), p(a(z4), p(a(y4), y5))))), P(b(z1), p(a(z3), p(a(z4), p(a(y4), y5)))))
P(a(z0), p(b(z1), p(a(z2), p(a(z3), p(a(z4), p(a(y4), p(a(y5), y6))))))) → c(P(z2, p(z3, p(z4, p(a(a(a(a(z0)))), p(b(z1), p(a(y4), p(a(y5), y6))))))), P(a(a(z0)), p(b(z1), p(a(z3), p(a(z4), p(a(y4), p(a(y5), y6)))))), P(b(z1), p(a(z3), p(a(z4), p(a(y4), p(a(y5), y6))))))

(12) Obligation:

Complexity Dependency Tuples Problem
Rules:

p(a(z0), p(b(z1), p(a(z2), z3))) → p(z2, p(a(a(z0)), p(b(z1), z3)))
Tuples:

P(a(z0), p(b(z1), p(a(z2), p(a(z3), p(a(y3), p(a(y4), y5)))))) → c(P(a(a(z0)), p(b(z1), p(a(z3), p(a(y3), p(a(y4), y5))))))
P(a(z0), p(b(z1), p(a(z2), p(a(z3), p(a(y3), y4))))) → c(P(a(a(z0)), p(b(z1), p(a(z3), p(a(y3), y4)))))
P(a(z0), p(b(z1), p(a(a(y0)), p(a(z3), p(a(z4), z5))))) → c(P(a(y0), p(z3, p(z4, p(a(a(a(a(z0)))), p(b(z1), z5))))), P(a(a(z0)), p(b(z1), p(a(z3), p(a(z4), z5)))), P(b(z1), p(a(z3), p(a(z4), z5))))
P(a(z0), p(b(z1), p(a(z2), p(a(z3), p(a(z4), p(a(y4), y5)))))) → c(P(z2, p(z3, p(z4, p(a(a(a(a(z0)))), p(b(z1), p(a(y4), y5)))))), P(a(a(z0)), p(b(z1), p(a(z3), p(a(z4), p(a(y4), y5))))), P(b(z1), p(a(z3), p(a(z4), p(a(y4), y5)))))
P(a(z0), p(b(z1), p(a(z2), p(a(z3), p(a(z4), p(a(y4), p(a(y5), y6))))))) → c(P(z2, p(z3, p(z4, p(a(a(a(a(z0)))), p(b(z1), p(a(y4), p(a(y5), y6))))))), P(a(a(z0)), p(b(z1), p(a(z3), p(a(z4), p(a(y4), p(a(y5), y6)))))), P(b(z1), p(a(z3), p(a(z4), p(a(y4), p(a(y5), y6))))))
S tuples:

P(a(z0), p(b(z1), p(a(z2), p(a(z3), p(a(y3), p(a(y4), y5)))))) → c(P(a(a(z0)), p(b(z1), p(a(z3), p(a(y3), p(a(y4), y5))))))
P(a(z0), p(b(z1), p(a(z2), p(a(z3), p(a(y3), y4))))) → c(P(a(a(z0)), p(b(z1), p(a(z3), p(a(y3), y4)))))
P(a(z0), p(b(z1), p(a(a(y0)), p(a(z3), p(a(z4), z5))))) → c(P(a(y0), p(z3, p(z4, p(a(a(a(a(z0)))), p(b(z1), z5))))), P(a(a(z0)), p(b(z1), p(a(z3), p(a(z4), z5)))), P(b(z1), p(a(z3), p(a(z4), z5))))
P(a(z0), p(b(z1), p(a(z2), p(a(z3), p(a(z4), p(a(y4), y5)))))) → c(P(z2, p(z3, p(z4, p(a(a(a(a(z0)))), p(b(z1), p(a(y4), y5)))))), P(a(a(z0)), p(b(z1), p(a(z3), p(a(z4), p(a(y4), y5))))), P(b(z1), p(a(z3), p(a(z4), p(a(y4), y5)))))
P(a(z0), p(b(z1), p(a(z2), p(a(z3), p(a(z4), p(a(y4), p(a(y5), y6))))))) → c(P(z2, p(z3, p(z4, p(a(a(a(a(z0)))), p(b(z1), p(a(y4), p(a(y5), y6))))))), P(a(a(z0)), p(b(z1), p(a(z3), p(a(z4), p(a(y4), p(a(y5), y6)))))), P(b(z1), p(a(z3), p(a(z4), p(a(y4), p(a(y5), y6))))))
K tuples:none
Defined Rule Symbols:

p

Defined Pair Symbols:

P

Compound Symbols:

c, c

(13) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID) transformation)

Use forward instantiation to replace P(a(z0), p(b(z1), p(a(z2), p(a(z3), p(a(y3), y4))))) → c(P(a(a(z0)), p(b(z1), p(a(z3), p(a(y3), y4))))) by

P(a(z0), p(b(z1), p(a(z2), p(a(z3), p(a(z4), p(a(y4), p(a(y5), y6))))))) → c(P(a(a(z0)), p(b(z1), p(a(z3), p(a(z4), p(a(y4), p(a(y5), y6)))))))
P(a(z0), p(b(z1), p(a(z2), p(a(z3), p(a(z4), p(a(y4), y5)))))) → c(P(a(a(z0)), p(b(z1), p(a(z3), p(a(z4), p(a(y4), y5))))))
P(a(z0), p(b(z1), p(a(z2), p(a(a(y2)), p(a(z4), p(a(y4), y5)))))) → c(P(a(a(z0)), p(b(z1), p(a(a(y2)), p(a(z4), p(a(y4), y5))))))
P(a(z0), p(b(z1), p(a(z2), p(a(z3), p(a(z4), p(a(y4), p(a(y5), p(a(y6), y7)))))))) → c(P(a(a(z0)), p(b(z1), p(a(z3), p(a(z4), p(a(y4), p(a(y5), p(a(y6), y7))))))))

(14) Obligation:

Complexity Dependency Tuples Problem
Rules:

p(a(z0), p(b(z1), p(a(z2), z3))) → p(z2, p(a(a(z0)), p(b(z1), z3)))
Tuples:

P(a(z0), p(b(z1), p(a(z2), p(a(z3), p(a(y3), p(a(y4), y5)))))) → c(P(a(a(z0)), p(b(z1), p(a(z3), p(a(y3), p(a(y4), y5))))))
P(a(z0), p(b(z1), p(a(a(y0)), p(a(z3), p(a(z4), z5))))) → c(P(a(y0), p(z3, p(z4, p(a(a(a(a(z0)))), p(b(z1), z5))))), P(a(a(z0)), p(b(z1), p(a(z3), p(a(z4), z5)))), P(b(z1), p(a(z3), p(a(z4), z5))))
P(a(z0), p(b(z1), p(a(z2), p(a(z3), p(a(z4), p(a(y4), y5)))))) → c(P(z2, p(z3, p(z4, p(a(a(a(a(z0)))), p(b(z1), p(a(y4), y5)))))), P(a(a(z0)), p(b(z1), p(a(z3), p(a(z4), p(a(y4), y5))))), P(b(z1), p(a(z3), p(a(z4), p(a(y4), y5)))))
P(a(z0), p(b(z1), p(a(z2), p(a(z3), p(a(z4), p(a(y4), p(a(y5), y6))))))) → c(P(z2, p(z3, p(z4, p(a(a(a(a(z0)))), p(b(z1), p(a(y4), p(a(y5), y6))))))), P(a(a(z0)), p(b(z1), p(a(z3), p(a(z4), p(a(y4), p(a(y5), y6)))))), P(b(z1), p(a(z3), p(a(z4), p(a(y4), p(a(y5), y6))))))
P(a(z0), p(b(z1), p(a(z2), p(a(z3), p(a(z4), p(a(y4), p(a(y5), y6))))))) → c(P(a(a(z0)), p(b(z1), p(a(z3), p(a(z4), p(a(y4), p(a(y5), y6)))))))
P(a(z0), p(b(z1), p(a(z2), p(a(a(y2)), p(a(z4), p(a(y4), y5)))))) → c(P(a(a(z0)), p(b(z1), p(a(a(y2)), p(a(z4), p(a(y4), y5))))))
P(a(z0), p(b(z1), p(a(z2), p(a(z3), p(a(z4), p(a(y4), p(a(y5), p(a(y6), y7)))))))) → c(P(a(a(z0)), p(b(z1), p(a(z3), p(a(z4), p(a(y4), p(a(y5), p(a(y6), y7))))))))
S tuples:

P(a(z0), p(b(z1), p(a(z2), p(a(z3), p(a(y3), p(a(y4), y5)))))) → c(P(a(a(z0)), p(b(z1), p(a(z3), p(a(y3), p(a(y4), y5))))))
P(a(z0), p(b(z1), p(a(a(y0)), p(a(z3), p(a(z4), z5))))) → c(P(a(y0), p(z3, p(z4, p(a(a(a(a(z0)))), p(b(z1), z5))))), P(a(a(z0)), p(b(z1), p(a(z3), p(a(z4), z5)))), P(b(z1), p(a(z3), p(a(z4), z5))))
P(a(z0), p(b(z1), p(a(z2), p(a(z3), p(a(z4), p(a(y4), y5)))))) → c(P(z2, p(z3, p(z4, p(a(a(a(a(z0)))), p(b(z1), p(a(y4), y5)))))), P(a(a(z0)), p(b(z1), p(a(z3), p(a(z4), p(a(y4), y5))))), P(b(z1), p(a(z3), p(a(z4), p(a(y4), y5)))))
P(a(z0), p(b(z1), p(a(z2), p(a(z3), p(a(z4), p(a(y4), p(a(y5), y6))))))) → c(P(z2, p(z3, p(z4, p(a(a(a(a(z0)))), p(b(z1), p(a(y4), p(a(y5), y6))))))), P(a(a(z0)), p(b(z1), p(a(z3), p(a(z4), p(a(y4), p(a(y5), y6)))))), P(b(z1), p(a(z3), p(a(z4), p(a(y4), p(a(y5), y6))))))
P(a(z0), p(b(z1), p(a(z2), p(a(z3), p(a(z4), p(a(y4), p(a(y5), y6))))))) → c(P(a(a(z0)), p(b(z1), p(a(z3), p(a(z4), p(a(y4), p(a(y5), y6)))))))
P(a(z0), p(b(z1), p(a(z2), p(a(a(y2)), p(a(z4), p(a(y4), y5)))))) → c(P(a(a(z0)), p(b(z1), p(a(a(y2)), p(a(z4), p(a(y4), y5))))))
P(a(z0), p(b(z1), p(a(z2), p(a(z3), p(a(z4), p(a(y4), p(a(y5), p(a(y6), y7)))))))) → c(P(a(a(z0)), p(b(z1), p(a(z3), p(a(z4), p(a(y4), p(a(y5), p(a(y6), y7))))))))
K tuples:none
Defined Rule Symbols:

p

Defined Pair Symbols:

P

Compound Symbols:

c, c

(15) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID) transformation)

Use forward instantiation to replace P(a(z0), p(b(z1), p(a(z2), p(a(z3), p(a(y3), p(a(y4), y5)))))) → c(P(a(a(z0)), p(b(z1), p(a(z3), p(a(y3), p(a(y4), y5)))))) by

P(a(z0), p(b(z1), p(a(z2), p(a(z3), p(a(z4), p(a(z5), p(a(y5), y6))))))) → c(P(a(a(z0)), p(b(z1), p(a(z3), p(a(z4), p(a(z5), p(a(y5), y6)))))))
P(a(z0), p(b(z1), p(a(z2), p(a(a(y2)), p(a(z4), p(a(z5), z6)))))) → c(P(a(a(z0)), p(b(z1), p(a(a(y2)), p(a(z4), p(a(z5), z6))))))
P(a(z0), p(b(z1), p(a(z2), p(a(z3), p(a(z4), p(a(z5), p(a(y5), p(a(y6), y7)))))))) → c(P(a(a(z0)), p(b(z1), p(a(z3), p(a(z4), p(a(z5), p(a(y5), p(a(y6), y7))))))))
P(a(z0), p(b(z1), p(a(z2), p(a(z3), p(a(a(y3)), p(a(z5), p(a(y5), y6))))))) → c(P(a(a(z0)), p(b(z1), p(a(z3), p(a(a(y3)), p(a(z5), p(a(y5), y6)))))))
P(a(z0), p(b(z1), p(a(z2), p(a(z3), p(a(z4), p(a(z5), p(a(y5), p(a(y6), p(a(y7), y8))))))))) → c(P(a(a(z0)), p(b(z1), p(a(z3), p(a(z4), p(a(z5), p(a(y5), p(a(y6), p(a(y7), y8)))))))))

(16) Obligation:

Complexity Dependency Tuples Problem
Rules:

p(a(z0), p(b(z1), p(a(z2), z3))) → p(z2, p(a(a(z0)), p(b(z1), z3)))
Tuples:

P(a(z0), p(b(z1), p(a(z2), p(a(z3), p(a(y3), p(a(y4), y5)))))) → c(P(a(a(z0)), p(b(z1), p(a(z3), p(a(y3), p(a(y4), y5))))))
P(a(z0), p(b(z1), p(a(a(y0)), p(a(z3), p(a(z4), z5))))) → c(P(a(y0), p(z3, p(z4, p(a(a(a(a(z0)))), p(b(z1), z5))))), P(a(a(z0)), p(b(z1), p(a(z3), p(a(z4), z5)))), P(b(z1), p(a(z3), p(a(z4), z5))))
P(a(z0), p(b(z1), p(a(z2), p(a(z3), p(a(z4), p(a(y4), y5)))))) → c(P(z2, p(z3, p(z4, p(a(a(a(a(z0)))), p(b(z1), p(a(y4), y5)))))), P(a(a(z0)), p(b(z1), p(a(z3), p(a(z4), p(a(y4), y5))))), P(b(z1), p(a(z3), p(a(z4), p(a(y4), y5)))))
P(a(z0), p(b(z1), p(a(z2), p(a(z3), p(a(z4), p(a(y4), p(a(y5), y6))))))) → c(P(z2, p(z3, p(z4, p(a(a(a(a(z0)))), p(b(z1), p(a(y4), p(a(y5), y6))))))), P(a(a(z0)), p(b(z1), p(a(z3), p(a(z4), p(a(y4), p(a(y5), y6)))))), P(b(z1), p(a(z3), p(a(z4), p(a(y4), p(a(y5), y6))))))
P(a(z0), p(b(z1), p(a(z2), p(a(z3), p(a(z4), p(a(y4), p(a(y5), y6))))))) → c(P(a(a(z0)), p(b(z1), p(a(z3), p(a(z4), p(a(y4), p(a(y5), y6)))))))
P(a(z0), p(b(z1), p(a(z2), p(a(a(y2)), p(a(z4), p(a(y4), y5)))))) → c(P(a(a(z0)), p(b(z1), p(a(a(y2)), p(a(z4), p(a(y4), y5))))))
P(a(z0), p(b(z1), p(a(z2), p(a(z3), p(a(z4), p(a(y4), p(a(y5), p(a(y6), y7)))))))) → c(P(a(a(z0)), p(b(z1), p(a(z3), p(a(z4), p(a(y4), p(a(y5), p(a(y6), y7))))))))
P(a(z0), p(b(z1), p(a(z2), p(a(z3), p(a(a(y3)), p(a(z5), p(a(y5), y6))))))) → c(P(a(a(z0)), p(b(z1), p(a(z3), p(a(a(y3)), p(a(z5), p(a(y5), y6)))))))
P(a(z0), p(b(z1), p(a(z2), p(a(z3), p(a(z4), p(a(z5), p(a(y5), p(a(y6), p(a(y7), y8))))))))) → c(P(a(a(z0)), p(b(z1), p(a(z3), p(a(z4), p(a(z5), p(a(y5), p(a(y6), p(a(y7), y8)))))))))
S tuples:

P(a(z0), p(b(z1), p(a(a(y0)), p(a(z3), p(a(z4), z5))))) → c(P(a(y0), p(z3, p(z4, p(a(a(a(a(z0)))), p(b(z1), z5))))), P(a(a(z0)), p(b(z1), p(a(z3), p(a(z4), z5)))), P(b(z1), p(a(z3), p(a(z4), z5))))
P(a(z0), p(b(z1), p(a(z2), p(a(z3), p(a(z4), p(a(y4), y5)))))) → c(P(z2, p(z3, p(z4, p(a(a(a(a(z0)))), p(b(z1), p(a(y4), y5)))))), P(a(a(z0)), p(b(z1), p(a(z3), p(a(z4), p(a(y4), y5))))), P(b(z1), p(a(z3), p(a(z4), p(a(y4), y5)))))
P(a(z0), p(b(z1), p(a(z2), p(a(z3), p(a(z4), p(a(y4), p(a(y5), y6))))))) → c(P(z2, p(z3, p(z4, p(a(a(a(a(z0)))), p(b(z1), p(a(y4), p(a(y5), y6))))))), P(a(a(z0)), p(b(z1), p(a(z3), p(a(z4), p(a(y4), p(a(y5), y6)))))), P(b(z1), p(a(z3), p(a(z4), p(a(y4), p(a(y5), y6))))))
P(a(z0), p(b(z1), p(a(z2), p(a(z3), p(a(z4), p(a(y4), p(a(y5), y6))))))) → c(P(a(a(z0)), p(b(z1), p(a(z3), p(a(z4), p(a(y4), p(a(y5), y6)))))))
P(a(z0), p(b(z1), p(a(z2), p(a(a(y2)), p(a(z4), p(a(y4), y5)))))) → c(P(a(a(z0)), p(b(z1), p(a(a(y2)), p(a(z4), p(a(y4), y5))))))
P(a(z0), p(b(z1), p(a(z2), p(a(z3), p(a(z4), p(a(y4), p(a(y5), p(a(y6), y7)))))))) → c(P(a(a(z0)), p(b(z1), p(a(z3), p(a(z4), p(a(y4), p(a(y5), p(a(y6), y7))))))))
P(a(z0), p(b(z1), p(a(z2), p(a(z3), p(a(a(y3)), p(a(z5), p(a(y5), y6))))))) → c(P(a(a(z0)), p(b(z1), p(a(z3), p(a(a(y3)), p(a(z5), p(a(y5), y6)))))))
P(a(z0), p(b(z1), p(a(z2), p(a(z3), p(a(z4), p(a(z5), p(a(y5), p(a(y6), p(a(y7), y8))))))))) → c(P(a(a(z0)), p(b(z1), p(a(z3), p(a(z4), p(a(z5), p(a(y5), p(a(y6), p(a(y7), y8)))))))))
K tuples:none
Defined Rule Symbols:

p

Defined Pair Symbols:

P

Compound Symbols:

c, c

(17) CpxTrsMatchBoundsTAProof (EQUIVALENT transformation)

A linear upper bound on the runtime complexity of the TRS R could be shown with a Match-Bound[TAB_LEFTLINEAR,TAB_NONLEFTLINEAR] (for contructor-based start-terms) of 0.

The compatible tree automaton used to show the Match-Boundedness (for constructor-based start-terms) is represented by:
final states : [1]
transitions:
a0(0) → 0
b0(0) → 0
p0(0, 0) → 1

(18) BOUNDS(O(1), O(n^1))